p:FinProbSpace, n, m:. (n  m)  (X:RandomVariable(p;n). E(n;X) = E(m;X)  ) 

latex

Definitions

n - m, n+m, -n, i  j , FinProbSpace, , s = t, , <a, b>, E(n;F), RandomVariable(p;n), A, False, P  Q, Void, a < b, #$n, A  B, x:AB(x), {x:A| B(x)} , x:A. B(x), t  T, , (i = j), f(a), null, SQType(T), {T}, s ~ t, T, True, Outcome, x,y. t(x;y), , qeq(r;s), tt, EquivRel(T;x,y.E(x;y)), if b then t else f fi , A  B, , , i  j < k, x:A  B(x), Type, {i..j}, ||as||, x,y:A//B(x;y), P & Q, S  T, type List, Top, x:A.B(x), suptype(S; T), left + right, Unit, P  Q, b, b, weighted-sum(p;F), x.A(x), rv-shift(x;X),

Lemmas

rv-shift wf, expectation wf, weighted-sum wf2, assert wf, not wf, bnot wf, eq int wf, assert of eq int, not functionality wrt iff, assert of bnot, iff transitivity, eqff to assert, eqtt to assert, rationals wf, top wf, length wf nat, int seg wf, null-seq wf, int nzero wf, b-union wf, btrue wf, qeq wf2, bool wf, quotient wf, int-rational, p-outcome wf, true wf, squash wf, subtype rel function, expectation-constant, nat wf, le wf, random-variable wf, finite-prob-space wf, nat properties, ge wf